Example 14 in [Alpuente, Escobar, Gramlich, and Lucas - LPAR'02, Example 14]

Summary: Ex14_AEGL02

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (non-terminating)
• Positive results:
  1. Polynomial interpretation (Modular decomposition @ MuTerm)
  2. Giesl and Middeldorp's transformation (CiME)
  3. CSRPO
  4. CSDP

CS-TRS Ex14_AEGL02 (file Ex14_AEGL02.csr)

Showing the CS-TRS  Ex14_AEGL02:


Functions:  from cons s length nil 0 length1

Constructors:  cons s nil 0

Variables:  X Y

Arities: 

ar(from) = 1
ar(cons) = 2
ar(s) = 1
ar(length) = 1
ar(nil) = 0
ar(0) = 0
ar(length1) = 1

Replacement map: 

µ(from)={1}
µ(cons)={1}
µ(s)={1}
µ(length)={}
µ(nil)={}
µ(0)={}
µ(length1)={}

Rules:  (file Ex14_AEGL02)   

from(X) -> cons(X,from(s(X)))
length(nil) -> 0
length(cons(X,Y)) -> s(length1(Y))
length1(X) -> length(X)

The CS-TRS in OBJ format (file Ex14_AEGL02.obj):

obj Ex14_AEGL02 is
  sort S .
  op from : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op s : S -> S .
  op length : S -> S [strat (0)] .
  op nil : -> S .
  op 0 : -> S .
  op length1 : S -> S [strat (0)] .
  vars X Y : S .
  eq from(X) = cons(X,from(s(X))) .
  eq length(nil) = 0 .
  eq length(cons(X,Y)) = s(length1(Y)) .
  eq length1(X) = length(X) .
endo

Negative results

1. The µ-termination of Ex14_AEGL02 cannot be proved by using Lucas' transformation. The TRS Ex14_AEGL02_L:

       from(X) -> cons(X)
       length -> 0
       length -> s(length1)
       length1 -> length
       

   is not terminating.

Positive results

1. The µ-termination of Ex2_Luc02a can be proved by using the following modular decomposition (computed by MuTerm):

   obj Ex14_AEGL02_1 is
     sort S .
     op from : S -> S .
     op cons : S S -> S [strat (1 0)] .
     op s : S -> S .
     vars X : S .
     eq from(X) = cons(X,from(s(X))) .
   endo
   

   and

   obj Ex14_AEGL02_2 is
     sort S .
     op length : S -> S [strat (0)] .
     op cons : S S -> S [strat (1 0)] .
     op s : S -> S .
     op length1 : S -> S [strat (0)] .
     op nil : -> S .
     op 0 : -> S .
     vars X Y : S .
     eq length(cons(X,Y)) = s(length1(Y)) .
     eq length(nil) = 0 .
     eq length1(X) = length(X) .
   endo
   

   The modules Ex14_AEGL02_1 and Ex14_AEGL02_2 can be proved terminating by using the following polynomial interpretations (computed with MuTerm):

       Proof of termination for Ex14_AEGL02_1:
   
       [from](X) = X + 1
       [cons](X1,X2) = X1
       [s](X) = X
       

   and

      Proof of termination for Ex14_AEGL02_2:
   
      [length](X) = X
      [cons](X1,X2) = X1 + X2 + 2
      [s](X) = X
      [length1](X) = X + 1
      [nil] = 1
      [0] = 0
      

2. The µ-termination of Ex14_AEGL02 can be proved by using Giesl and Middeldorp's transformation. The TRSs Ex14_AEGL02_GM:

       a__from(X) -> cons(mark(X),from(s(X)))
       a__length(nil) -> 0
       a__length(cons(X,Y)) -> s(a__length1(Y))
       a__length1(X) -> a__length(X)
       mark(from(X)) -> a__from(mark(X))
       mark(length(X)) -> a__length(X)
       mark(length1(X)) -> a__length1(X)
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       mark(s(X)) -> s(mark(X))
       mark(nil) -> nil
       mark(0) -> 0
       a__from(X) -> from(X)
       a__length(X) -> length(X)
       a__length1(X) -> length1(X)
       

   which result from the previous modular decomposition are terminating (use CiME).
3. The µ-termination of Ex14_AEGL02 can also be proved by using CSRPO (computed by MuTerm).
4. The µ-termination of Ex14_AEGL02 can also be proved by using CSDP (computed by MuTerm).